The architecture of a software defined networking (SDN) network is divided into three logical planes: (1) an application plane that hosts network applications, (2) a control plane that implements instances of a distributed network operating system, (3) a data plane that includes hosts and switches. The control plane generates rules that are provided to the data plane, which uses the rules to determine how to route flows through the SDN network. For example, a network application in the application plane can request a connection between a source address and a destination address. An instance of the distributed network operating system in the control plane receives the request and generates a set of flow rules for routing the flow between the source and destination addresses. The control plane entity provides the set of flow rules to the hosts and switches in the data plane, where they are stored in flow tables that are used to route the flows.
Network applications can be dynamically deployed in real time in an operational SDN network, but deploying unreliable or insecure network applications poses significant risks to the SDN network. For example, event-driven applications such as a reactive application that forwards incoming connection requests from a source to a destination can crash an SDN network under high rates of incoming requests. The SDN network crash causes the SDN network to drop packets in existing flows and renders the SDN network unresponsive to new packets and connection requests. Event-driven applications can therefore compromise the reliability and performance of the SDN network, as well as compromising the security of the SDN network, e.g., by rendering the SDN network vulnerable to denial-of-service (DoS) attacks. Event-driven software executing in the control plane can present similar risks to the stability of the SDN network.
Model checking is conventionally used to verify code and detect bugs by examining all execution paths in the code up to a specified depth. For example, the code used to implement a network application can be represented as a tree including decision nodes that represent each branch point (e.g., an if-then-else statement or thread scheduling choices) in the execution of the code. The model checking algorithm executes all paths through the tree up to a depth that can be specified by the number of decision nodes. For example, model checking code such as NASA's Java Path Finder follows every execution path in a program using backtracking. The backtracking algorithm includes saving the complete state of the program at every non-deterministic point (such as branch points) and then recursively exploring all alternative choices at the non-deterministic points after the termination of each execution path.